Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		filter(cons(X,Y),0,M)	→ cons(0,n__filter(activate(Y),M,M))
2:		filter(cons(X,Y),s(N),M)	→ cons(X,n__filter(activate(Y),N,M))
3:		sieve(cons(0,Y))	→ cons(0,n__sieve(activate(Y)))
4:		sieve(cons(s(N),Y))	→ cons(s(N),n__sieve(filter(activate(Y),N,N)))
5:		nats(N)	→ cons(N,n__nats(s(N)))
6:		zprimes	→ sieve(nats(s(s(0))))
7:		filter(X1,X2,X3)	→ n__filter(X1,X2,X3)
8:		sieve(X)	→ n__sieve(X)
9:		nats(X)	→ n__nats(X)
10:		activate(n__filter(X1,X2,X3))	→ filter(X1,X2,X3)
11:		activate(n__sieve(X))	→ sieve(X)
12:		activate(n__nats(X))	→ nats(X)
13:		activate(X)	→ X

There are 10 dependency pairs:


14:		FILTER(cons(X,Y),0,M)	→ ACTIVATE(Y)
15:		FILTER(cons(X,Y),s(N),M)	→ ACTIVATE(Y)
16:		SIEVE(cons(0,Y))	→ ACTIVATE(Y)
17:		SIEVE(cons(s(N),Y))	→ FILTER(activate(Y),N,N)
18:		SIEVE(cons(s(N),Y))	→ ACTIVATE(Y)
19:		ZPRIMES	→ SIEVE(nats(s(s(0))))
20:		ZPRIMES	→ NATS(s(s(0)))
21:		ACTIVATE(n__filter(X1,X2,X3))	→ FILTER(X1,X2,X3)
22:		ACTIVATE(n__sieve(X))	→ SIEVE(X)
23:		ACTIVATE(n__nats(X))	→ NATS(X)

The approximated dependency graph contains one SCC: {14-18,21,22}.

Consider the SCC {14-18,21,22}. The usable rules are {1-5,7-13}. The constraints could not be solved.

Tyrolean Termination Tool (17.96 seconds) --- May 3, 2006